↳ Prolog
↳ PrologToPiTRSProof
flat_in_ga(niltree, nil) → flat_out_ga(niltree, nil)
flat_in_ga(tree(X, niltree, T), cons(X, Xs)) → U1_ga(X, T, Xs, flat_in_ga(T, Xs))
flat_in_ga(tree(X, tree(Y, T1, T2), T3), Xs) → U2_ga(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
U2_ga(X, Y, T1, T2, T3, Xs, flat_out_ga(tree(Y, T1, tree(X, T2, T3)), Xs)) → flat_out_ga(tree(X, tree(Y, T1, T2), T3), Xs)
U1_ga(X, T, Xs, flat_out_ga(T, Xs)) → flat_out_ga(tree(X, niltree, T), cons(X, Xs))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
flat_in_ga(niltree, nil) → flat_out_ga(niltree, nil)
flat_in_ga(tree(X, niltree, T), cons(X, Xs)) → U1_ga(X, T, Xs, flat_in_ga(T, Xs))
flat_in_ga(tree(X, tree(Y, T1, T2), T3), Xs) → U2_ga(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
U2_ga(X, Y, T1, T2, T3, Xs, flat_out_ga(tree(Y, T1, tree(X, T2, T3)), Xs)) → flat_out_ga(tree(X, tree(Y, T1, T2), T3), Xs)
U1_ga(X, T, Xs, flat_out_ga(T, Xs)) → flat_out_ga(tree(X, niltree, T), cons(X, Xs))
FLAT_IN_GA(tree(X, niltree, T), cons(X, Xs)) → U1_GA(X, T, Xs, flat_in_ga(T, Xs))
FLAT_IN_GA(tree(X, niltree, T), cons(X, Xs)) → FLAT_IN_GA(T, Xs)
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3), Xs) → U2_GA(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3), Xs) → FLAT_IN_GA(tree(Y, T1, tree(X, T2, T3)), Xs)
flat_in_ga(niltree, nil) → flat_out_ga(niltree, nil)
flat_in_ga(tree(X, niltree, T), cons(X, Xs)) → U1_ga(X, T, Xs, flat_in_ga(T, Xs))
flat_in_ga(tree(X, tree(Y, T1, T2), T3), Xs) → U2_ga(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
U2_ga(X, Y, T1, T2, T3, Xs, flat_out_ga(tree(Y, T1, tree(X, T2, T3)), Xs)) → flat_out_ga(tree(X, tree(Y, T1, T2), T3), Xs)
U1_ga(X, T, Xs, flat_out_ga(T, Xs)) → flat_out_ga(tree(X, niltree, T), cons(X, Xs))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
FLAT_IN_GA(tree(X, niltree, T), cons(X, Xs)) → U1_GA(X, T, Xs, flat_in_ga(T, Xs))
FLAT_IN_GA(tree(X, niltree, T), cons(X, Xs)) → FLAT_IN_GA(T, Xs)
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3), Xs) → U2_GA(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3), Xs) → FLAT_IN_GA(tree(Y, T1, tree(X, T2, T3)), Xs)
flat_in_ga(niltree, nil) → flat_out_ga(niltree, nil)
flat_in_ga(tree(X, niltree, T), cons(X, Xs)) → U1_ga(X, T, Xs, flat_in_ga(T, Xs))
flat_in_ga(tree(X, tree(Y, T1, T2), T3), Xs) → U2_ga(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
U2_ga(X, Y, T1, T2, T3, Xs, flat_out_ga(tree(Y, T1, tree(X, T2, T3)), Xs)) → flat_out_ga(tree(X, tree(Y, T1, T2), T3), Xs)
U1_ga(X, T, Xs, flat_out_ga(T, Xs)) → flat_out_ga(tree(X, niltree, T), cons(X, Xs))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3), Xs) → FLAT_IN_GA(tree(Y, T1, tree(X, T2, T3)), Xs)
FLAT_IN_GA(tree(X, niltree, T), cons(X, Xs)) → FLAT_IN_GA(T, Xs)
flat_in_ga(niltree, nil) → flat_out_ga(niltree, nil)
flat_in_ga(tree(X, niltree, T), cons(X, Xs)) → U1_ga(X, T, Xs, flat_in_ga(T, Xs))
flat_in_ga(tree(X, tree(Y, T1, T2), T3), Xs) → U2_ga(X, Y, T1, T2, T3, Xs, flat_in_ga(tree(Y, T1, tree(X, T2, T3)), Xs))
U2_ga(X, Y, T1, T2, T3, Xs, flat_out_ga(tree(Y, T1, tree(X, T2, T3)), Xs)) → flat_out_ga(tree(X, tree(Y, T1, T2), T3), Xs)
U1_ga(X, T, Xs, flat_out_ga(T, Xs)) → flat_out_ga(tree(X, niltree, T), cons(X, Xs))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3), Xs) → FLAT_IN_GA(tree(Y, T1, tree(X, T2, T3)), Xs)
FLAT_IN_GA(tree(X, niltree, T), cons(X, Xs)) → FLAT_IN_GA(T, Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
FLAT_IN_GA(tree(X, niltree, T)) → FLAT_IN_GA(T)
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3)) → FLAT_IN_GA(tree(Y, T1, tree(X, T2, T3)))
No rules are removed from R.
FLAT_IN_GA(tree(X, niltree, T)) → FLAT_IN_GA(T)
FLAT_IN_GA(tree(X, tree(Y, T1, T2), T3)) → FLAT_IN_GA(tree(Y, T1, tree(X, T2, T3)))
POL(FLAT_IN_GA(x1)) = 2·x1
POL(niltree) = 0
POL(tree(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof